Storm-static - embedded up

Execution

Walltime:	0.09992694854736328s
Return code:	0
Note(s):	The tool result '477552373584969927833299/1000000000000000000000' is tagged as incorrect. The reference result is '2183712773184130223598585872047520914488122175606934413903652607811561354541768913273394354150731596243786927117080619972936950933211228822230841017997848035457022536274593694325272937241879112565615452852140040009951110511770453046543602028627759596040876523886281630666909773052679046752196663274749329033495803800223198189977967895274338342496880178318697600470928721863593921368994665022069121923146546749427668869964179406259239705083017079579837316334742438858110597273866404643748527627914035116439622241157884116961455558671646185889750342528436238819022600572834920059281639088233591813067367421725249678046731861054937584690961772718156792664262887588824125917593642808076083267656920293627884196441644507495997854599477443119950196357101319485841624585826437019347618526086759800865732832037553466875466901270734879681407694933108066741180927470524584064389847936646278385013902360895901588016440821591943708613991669538852289652630132790905572134555253789490170005059168185665735052259819770041185303718289878778733406203858246157516444569077120019044145792179148606591105921542067443616924426969193479216839640914514154579330293019916470242897744026812602435662758109157949491075995140783550947236459449746329029215408581508993471668737066067881412164151610804199376708900085509035917841621864138944467290829749417433364929282708907841113027796302533141416770846531202150706514206313094666476596182227170154073034763886586094848742289864106641847262258742294448432880789623129784063411053896323208255462396749474153327589093919489124624553290752885960034489080881223998694665884845850447400494028940797032167745880449766472598409304959825700121500595149639222970342012823184365995869663223168776955822675915520168/4572718918340297992861016207266988509138560572823306848829665424299052227511873796991915409911235818972613004530700672685720698204908764538720326409442926127700951433649408201112092564941380998921576941109250837022494566413393941205188626245721168194140412481054847774404826156318173828592036089336096893561020367354804146432102768640678989122018616511998302777619511228565811485630854571393462819833401567338208035372513671797820811573609314840372672325014146693231179799484153817835593205819002122730433616769967049004357596176219036811262970850919468802314953770502798139191686172212028575730678568621667225640320101421011723756204037351428553435160154128692425948580716062203995704926949659596847047937901467330759606876888282528724729065409076658690813670837079680607659220497177491416940645062309893908652700575386295070426625114918423310586794730384254548668064566827365948822329779522453464872939600768481953319487750588147872980488463406012059924520051494441241400216424433553966775513192672039779506357066648405600713809047919861717117847607341961357554333526306960152722611944383372658119891157778850950172371721016793258709192064299305689622465056677801811031340215436851137792601061271941765262648293155902813064195440251739408021071721765433252009902890909464534701229221329432016138637206311482312570698044605998411197506803148471038371352304706209604224183783179520545733608106657737510279107506655719879117689898747777725608137653857013035855106110221663018957239214900397934041851769373159388703677025445608492463824370974258226639989548083202480591870877671674507734785725257431651992424103523845692631201850480374173032425261397494887570649149902839082330582151102087170601721708405579348599375587665625' (approx. 477.55237358361944) which means a relative error of '2.8279177365483827e-12' which is larger than the goal precision '1e-14'.
Relative Error:	2.8279177365483827e-12

Log

Storm 1.5.1

Date: Tue Apr 28 17:19:14 2020
Command line arguments: --prism embedded.prism --prop embedded.props up_time --constants 'MAX_COUNT=8,T=12' --prismcompat --exact floats '--general:precision' 1e-20 --ddlib sylvan '--sylvan:maxmem' 6114 '--sylvan:threads' 4 --engine sparse
Current working directory: /

 WARN (GeneralSettings.cpp:110): Setting the precision option with module prefix does not effect all solvers. Consider setting --precision instead of --general:precision.
 WARN (Program.cpp:178): The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Consider rewriting the commands to use Markovian commands instead.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
Time for model input parsing: 0.004s.

 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
Time for model construction: 0.057s.

-------------------------------------------------------------- 
Model type: 	CTMC (sparse)
States: 	5820
Transitions: 	16788
Reward Models:  up
State Labels: 	3 labels
   * deadlock -> 0 item(s)
   * down -> 3156 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "up_time": R[exp]{"up"}=? [F "down"] ...
Result (for initial states): 477.552373584969927833299
Time for model checking: 0.009s.

Model:	embedded v.1 (CTMC)
Parameter(s)	MAX_COUNT = 8, T = 12
Property:	up_time (exp-reward)